% $Revision$
% $Id$


\chapter{Declarations and Bindings} \label{declarations}
\index{module!declaration} \index{declaration} \index{declaration!module}

In this chapter, we describe the syntax and informal semantics of \frege{} \emph{declarations}.

\begin{flushleft}
\rul{program} \term{module} \nont{modulename} \opt{\nont{inline}} \term{where} \bracea{} \nont{body} \bracez{} \label{moduledcl} \\
%  \alt \term{module} \nont{modulename} \sym{;} \nont{body} \\
\rul{modulename} \nont{qconid}
  \alt \nont{qvarid} \sym{.} \nont{modulename}
  \alt \nont{qconid} \sym{.} \nont{modulename}\\
\rul{inline} \term{inline} \sym{(} \liste{\nont{qname}}{\sym{,}} \sym{)}\\
\rul{body} \nont{topdecl}
  \alt \nont{topdecl} \sym{;} \nont{body}\\
\rul{topdecl} \nont{fixity} \gcom{see \autoref{fixity}}
  \alt \nont{importdcl}        \gcom{\hyperref[import]{import declaration}}
  \alt \nont{typedcl}          \gcom{\hyperref[typedcl]{type alias declaration}}
  \alt \nont{datadcl}          \gcom{\hyperref[algdcl]{data type declaration}}
  \alt \nont{classdcl}         \gcom{type class declaration}
  \alt \nont{instdcl}          \gcom{instance declaration}
  \alt \nont{derivedcl}        \gcom{derived instance declaration}
  \alt \nont{decl}\\
\rul{decl} \nont{annotation}    \gcom{type annotation}
  \alt  \nont{binding}          \gcom{function or pattern binding}
  \alt  \nont{nativefun}        \gcom{native function}\\
\rul{decls} \liste{\nont{decl}}{\sym{;}}\\

\end{flushleft}

The \emph{modulename} is a sequence of one or more identifiers where the last identifier starts with an uppercase letter.
The module declaration opens a namespace with a name that equals the last component of the module name.
Each top level item can be accessed with a qualified name that uses the namespace as qualifier, thus in\exq{
module my.fine.pack.with.a.long.name.X where\\
foo = 42\\
bar = let foo = 24 in foo + X.foo
}
\texttt{bar} evaluates to 66.

\index{declaration!top level}

The \emph{body} is a list of top level declarations. It is immaterial in which order the declarations are given.

The declarations in the syntactic category \nont{topdecl} are only allowed at the top level of a \frege{} module, whereas \nont{decl}s can be used either at the top level or in the scope of a data type, class or instance.

Every top level declaration except fixity and import declarations can be preceded by one of the keywords \term{private}, \term{protected} or \term{public}, where \term{public} is the default and hence redundant. This determines the visibility of the declared item in importing modules. For detailed discussion of import and export see \autoref{import}.

For exposition, we divide the declarations into three groups: user defined data types, consisting of type and data declarations; type classes and overloading, consisting of class and instance declarations; and nested declarations, consisting of value bindings and type signatures.

\subsection*{Inline candidates}

The \term{inline} clause in the module declaration causes the named items to become candidates for inlining. Inlineable functions may not:

\begin{itemize}
\item contain a let or where clause
\item contain non-exhaustive patterns in lambda or case expressions
\item be recursive
\item reference private top level items
\end{itemize}

If these conditions are not met by a certain item, a warning will appear and the item will be ignored.

Note that all default class operations are automatically inline candidates.

If some module later imports the current module, the source code of the inlineable functions will be available and if the compiler options demand it, full applications of the said functions will be inlined.

For example, the (\sym{\$}) operator is an inline candidate of the Prelude and an application \ex{
f \$ a}
will be rewritten as \ex{f a} if the compiler was instructed to do inlining.


\section{Overview of Types and Classes}
\frege{} uses an polymorphic type system based on the traditional Hindley-Milner type system \cite{ptifart} to provide a static type semantics. The type system supports \emph{type classes} or just \emph{classes} that provide a structured way to introduce \emph{overloaded} functions and values.

A \texttt{class} declaration (\autoref{classdcl}) introduces a new \emph{type class} and the overloaded operations that must be supported by any type that is an \emph{instance}\label{instance} of that class. An \texttt{instance} declaration (\autoref{instdcl}) declares that a type is an \emph{instance} of a class and includes the definitions of the overloaded operations - called \emph{class methods} - instantiated on the named type. \index{class} \index{instance}

\java{} programmers are familiar with the concept of \emph{interfaces} which serve a similar purpose like \emph{type classes}, but there is a fundamental difference: A \frege{} type class is not a type in its own right like a \java{} interface. Instances of type classes are types, instances of \java{} interfaces are objects.

\subsection{Kinds}

To ensure that they are valid, type expressions are classified into different \emph{kinds}, which take one of two possible forms:

\begin{itemize}
\item The symbol \sym{*} represents the kind of all nullary type constructors.

\item If $k_1$ and $k_2$ are kinds, then $k_1$ \arrow{} $k_2$ is the kind of types that take a type of kind $k_1$ and return a type of kind $k_2$.

\end{itemize}

Kind inference checks the validity of type expressions in a similar way that type inference checks the validity of value expressions. However, it is also allowed to state the kind of type variables explicitly, as long as the given kind is compatible with what kind inference would have inferred.

\subsection{Syntax of Types} \index{type} \index{type!syntax} \label{typesyntax}

The syntax for \frege{} type expressions is given below. Just as data values are built using data constructors, type values are built from \emph{type constructors}. As with data constructors the names of type constructors start with uppercase letters.

The names of type constructors and data constructors will never be confused (by the compiler, that is) as the former only appear in expressions in the form of qualifiers and the latter never appear in types.

\begin{flushleft}
\rul{sigma} \term{forall} \liste{\nont{tyvar}}{} \sym{.} \nont{crho} \gcom{quantified type}
   \alt{} \nont{crho} \\
\rul{crho} \nont{constraints} \sym {=>} \nont{rho}  \gcom{constrained type} \alt{} \nont{rho}\\
\rul{rho} \sym{(} \nont{sigma} \sym{)} \sym{\arrow{}} \nont{rho} \gcom{higher ranked function type} 
  \alt{} \nont{tyapp} \sym{\arrow{}} \nont{rho}                           \gcom{function type}
  \alt{} \nont{tyapp} \\
\rul{constraints} \nont{constraint} 
	\alt{} \sym{(} \liste{\nont{constraint}}{\sym{,}} \sym{)} \label{constraint}\\
\rul{constraint} \nont{classname} \liste{\nont{tvapp}}{} \\
\rul{type} \nont{tyapp} \sym{\arrow{}} \nont{type} \gcom{function type}
  \alt \nont{tyapp}\\
\rul{tyapp} \nont{tyapp} \nont{simpletype}  \gcom{type application}
  \alt \nont{simpletype}\\
\rul{simpletype} \nont{tyvar} \gcom{type variable}
  \alt \nont{tycon}           \gcom{type constructor}
  \alt \sym{(} \nont{type} \sym{)}
  \alt \sym{(} \nont{type} \sym{,} \liste{\nont{type}}{\sym{,}} \sym{)} \gcom{\hyperref[tupletypes]{tuple types}}
  \alt \sym{\bracka{}} \nont{type} \sym{\brackz{}}  \gcom{\hyperref[listtype]{list type}}
  \alt \sym{(} \nont{type} \sym{|} \liste{\nont{type}}{\sym{|}} \sym{)} 
                                \gcom{\hyperref[nested-either]{nested \texttt{Either}}}\\
\rul{tyvar} \nont{varid} 
    \alt \sym{(}\nont{varid}\sym{::}\nont{kind}\sym{)}\\
\rul{tvapp} \nont{tyvar} 
  \alt{} \sym{(} \liste{\nont{tvapp}}{} \sym{)} \\
\rul{tycon} \nont{qconid}
  \alt \sym{\bracka\brackz}  \gcom{list type constructor}
  \alt \sym{()}              \gcom{unit type constructor}
  \alt \sym{(}\more{\sym{,}}\sym{)} \gcom{tuple type constructors}
  \alt $\rightarrow{}$ \gcom{function type constructor (infix operator)}\\
\rul{classname} \nont{qconid}\\
\rul{kind} \nont{simplekind}
  \alt \nont{simplekind} $\rightarrow{}$ \nont{kind}\\
\rul{simplekind} \sym{*} \alt \sym{(} \nont{kind} \sym{)}\\
\end{flushleft}

The main forms of type expressions are as follows:

\begin{enumerate}
\item Type variables written as identifiers beginning with a lowercase letter.  A type variable can stand for a type of any kind.
\item Type constructors. Type constructors are written as identifiers beginning with an uppercase letter. The identifiers may be qualified. Type constructors denote either a user defined data type or a type alias.

Special syntax is provided for the type constructors of the function type, list type, the trivial type and the tuple types.

Type constructors can be constants like \texttt{Int} that denotes the integer type or they can be polymorphic like the list type.
\item Type application. Polymorphic type constructors (or type variables that stand for them) must be applied to type parameters to denote a complete type. For example, the list type constructor requires a type for the elements of the list. 
\item A parenthesized type ($t$) is identical to the type $t$, but the parenthesis may be required for syntactical reasons.
\end{enumerate}

Special syntax is provided to allow certain type expressions to be written in a more traditional style:

\begin{enumerate}
\item A \emph{function type} has the form $t_1$ \arrow{} $t_2$. Function arrows associate to the right, thus $t_1$ \arrow{} ($t_2$ \arrow{} $t_3$) can be written $t_1$ \arrow{} $t_2$ \arrow{} $t_3$.

The function type constructor operator can be used in prefix form, that is $a$ \arrow{} $b$ is equivalent to (\arrow{}) $a$ $b$, as usual.

\item A \emph{tuple type} has the form ($t_1$, $\cdots$, $t_k$) where $k\ge{}2$, which is equivalent to the type (, $\cdots$,) $t_1$ $\cdots$ $t_k$ where there are $k-1$ commas between the parenthesis.
It denotes the type of $k$-tuples with the first component of type $t_1$, the second component of type $t_2$ and so on.
\item A \emph{list type} has the form $\bracka{}t\brackz{}$, which is equivalent to the type $\bracka{}\brackz{}$ $t$. It denotes the type of lists with elements of the type $t$.
\end{enumerate}

Although the tuple and list types have special syntax, they are not different from user-defined types with equivalent functionality.

Expressions, patterns and types have a consistent syntax. If $t_i$ is the type of expression or pattern $e_i$, then the expressions
($\backslash$ $e_1$ \arrow{} $e_2$),
$\bracka{}e_1\brackz{}$
and ($e_1$, $e_2$) have the types
($t_1$ \arrow{} $t_2$), $\bracka{}t_1\brackz{}$ and ($t_1$, $t_2$),
respectively.

In annotations, annotated expressions and patterns, the type variables in a type expression can be explicitly  quantified (see rule \nont{sigma}). In this case, it is a static error if a type variable that was not quantified appears in the type.
Absent an explicit \term{forall}, all type variables are assumed to be universally quantified. For example, the type expression \texttt{a \arrow{} a} denotes the type $\forall$ $a$.$a$ \arrow{} $a$.
For clarity, however, we'll sometimes write quantification explicitly when discussing the types of \frege{} programs.

More on explicit quantification is explained in the section dealing with \hyperref[higher-rank]{higher rank polymorphism}.

In type annotations as well as in class and instance declarations, the possible types represented by type variables (or applications of type variables) can be \hyperref[constraint]{constrained} to be members of a certain type class. 

\section{User-Defined Data Types} \index{data type}  \index{top level!declaration!data}

In this section, we describe algebraic and native data types (\texttt{data} declaration) and type synonyms (\texttt{type} declaration). These declarations may only appear at the top level of a module.

\subsection{Algebraic Data type Declaration} \index{data type!user defined} \index{data type!algebraic} \label{algdcl}

\begin{flushleft}
\rul{datadcl} \opt{\term{abstract}} \term{data} \nont{conid} \some{\nont{tyvar}} \sym{=} \nont{constructors} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}\\
\rul{constructors} \liste{\nont{constructor}}{\sym{$|$}}\\
\rul{constructor} \opt{\term{private}} \nont{conid} \some{\nont{simpletype}}\gcom{traditional constructor}
  \alt\ \opt{\term{private}}  \nont{conid} \bracea{} \liste{\nont{labels} :: \nont{sigma}}{,}\bracez{}\gcom{constructor with fields}\\
\rul{labels} \liste{\opt{\sym{!}}\nont{varid}}{,}\\
\end{flushleft}

An algebraic data type declaration introduces a new type and constructors for making values of that type and has the form:
\begin{quote}
\texttt{data} $T$ $u_1$ $\cdots$ $u_k$ \texttt{=} $K_1$ $t_{11}$ $\cdots$ $t_{1k_1}$ $|$ $\cdots$ $|$ $K_n$ $t_{n1}$ $\cdots$ $t_{nk_n}$
\end{quote}

This declaration introduces a new type constructor $T$ with constituent data constructors $K_1$, $\cdots$, $K_n$ whose types are given by
\begin{quote}
$\forall$ $u_1$ $\cdots$ $u_k$ . $t_{i1}$ \arrow{} $\cdots$ \arrow{} $t_{ik_i}$ \arrow{} $T$ $u_1$ $\cdots$ $u_k$
\end{quote}

The type variables $u_1$ through $u_k$ must be distinct and may appear in the $t_{ij}$; it is a static error for any other type variable to appear in the right hand side, except when said type variable is protected by a \term{forall} of a \hyperref[polyrf]{polymorphic record field}.

It is possible to reference the newly introduced type constructor $T$ on the right hand side of its own declaration, which allows to declare recursive types. For example, the following type is like the built-in list type:

\begin{code}
data List a = EmptyList | Cons a (List a)
\end{code}

The declaration can be read "A list of elements of type a is either the empty list or an element of type a "consed" to another list of elements of type a".

There are some special cases for user defined data types:
\begin{description}
\item [product types] are data types with exactly one constructor. The most prominent product types are tuples.
\item [enumerations] are data types where all constructors are constants, i.e. \exq{
data Color = Black | Red | Yellow}
\item [renamed types] \label{renamed-types} are product types where the constructor has exactly one field. Values of a renamed type will have the same representation as the constructor field at runtime, hence construction and deconstruction will incur no overhead. Yet at compile time renamed types are treated like any other algebraic data type.
\footnote{This is equivalent to Haskell's \term{newtype}.}
\end{description}

\subsubsection{Visibility of constructors and abstract data types}

The keyword \term{private} in front of a constructor declaration restricts the visibility of the constructor. Unqualified access is possible only from the declarations given in the \term{where} clause of the type. To access it in the rest of the module, the constructor name must be qualified with the type name. In other modules, the constructor is not visible at all.

The keyword \term{abstract} before a data declaration is equivalent to making all constructors private.

\subsubsection{Strict or Eager Constructors}

The default behavior for constructor applications is that the arguments are not evaluated. Evaluation will only take place when a value is deconstructed and a field value so obtained must be evaluated. Hence, operationally, a data structure does not store values but closures.

Sometimes a stricter mode is desired. A \sym{!} before a field name requires that the constructor shall be strict in the corresponding argument. It is possible to have some, none, or all fields strict. Lazy and strict constructors can be mixed in one and the same data type.

\subsubsection{Constructors with labeled fields} \label{fieldconstructor}

A different form for constructors is

\begin{quote}
$K_j$ \bracea{} $f_{j1}$ :: $t_{j1}$, $\cdots$, $f_{j{k_j}}$ :: $t_{j{k_j}}$ \bracez{}
\end{quote}

where the $f_ji$ are field labels and the $t_ji$ are the types.

\label{polyrf} The type of a labeled field can be \emph{polymorphic}, that is, it may mention type variables in a \term{forall}-type that are not type parameters of the type constructor.

\example{\tt
\begin{flushleft}
data F = F \bracea{} fun :: forall a . \bracka{}a\brackz{} $\rightarrow{}$ \bracka{}a\brackz{} \bracez{}\\
~\\

bar F\bracea{}fun\bracez{} = (fun \bracka{}0,1\brackz{}, fun \bracka{}true, false\brackz{})\\
\end{flushleft}
}

As before, the type of the constructor is

\begin{quote}
$\forall$ $u_1$ $\cdots$ $u_k$ . $t_{j1}$ \arrow{} $\cdots$ \arrow{} $t_{jk_j}$ \arrow{} $T$ $u_1$ $\cdots$ $u_k$
\end{quote}

Any number of constructors of an algebraic data type can employ the field list syntax. 
Constructors with and without field lists can be mixed.
For convenience, when consecutive fields have the same type, they can be grouped so that the type must be written only once.

\trans{
\begin{flushleft}
\textbf{data} T = $\cdots$ $|$  D \bracea{}$f_{a1}, f_{a2}, f_{a3}$ :: $t_{a}$, $f_{b1}$ :: $t_{b}$ \bracez{} $|$ $\cdots$\\
\end{flushleft}
translates to
\begin{flushleft}
\textbf{data} T = $\cdots$ $|$  D \bracea{}$f_{a1}, $ :: $t_{a}$, $f_{a2}, $ :: $t_{a}$, $f_{a3}, $ :: $t_{a}$, $f_{b1}$ :: $t_{b}$ \bracez{} $|$ $\cdots$\\
\end{flushleft}
}


Every field in one and the same constructor must have a different label, but the same label can appear in a different constructor of the same \term{data} definition. 
All fields with the same label that appear in the same \term{data} definition must have the same type.

\hasdiff{The same field label with a possibly different type can appear in constructors of other types. 
This is because field names are only known locally in the type whose constructor introduced them. 
A name given to a field can thus in addition be used for a global variable.}

For every field label appearing in an algebraic data type, 
the compiler defines automatically functions that extract a field from a value,
update or change a field in a value
\footnote{This is, of course, nondestructive update, i.e. a new value that differs only in the value for the field is created.} 
and check, if the given value has a certain field.


\trans{
\begin{flushleft}
\textbf{data} T = A $t_{a}$ $|$  B \bracea{}$f_{ba}$ :: $t_{ba}$, $f_{bc}$ :: $t_{bc}$ \bracez{} $|$ C \bracea{}$f_{bc}$ :: $t_{bc}$, $f_c$ :: $t_c$\bracez{}\\
\end{flushleft}
translates to
\begin{flushleft}
\textbf{data} T = A $t_a$ $|$  B $t_b$  $t_{bc}$ $|$ C $t_{bc}$ $t_c$ \textbf{where}\\
\hspace{0.3in}// For each of the fields $f_b$, $f_ {bc}$ and $f_c$,  4 functions will be generated,\\ 
\hspace{0.3in}// we give here exemplary the ones for $f_{bc}$\\
\hspace{0.3in}$f_{bc}$ $v$ = \textbf{case} $v$ \textbf{of}\\
\hspace{0.5in}\bracea{} B \_ $f$ $\rightarrow$ $f$; C $f$ \_ $\rightarrow$ $f$ \bracez{}\\
\hspace{0.3in}upd$f_{bc}$ $v$ $u$ = \textbf{case} $v$ \textbf{of}\\
\hspace{0.5in}\bracea{} B $a$ \_ $\rightarrow$ B $a$ $u$; C \_ $a$ $\rightarrow$ C $u$ $a$ \bracez{}\\
\hspace{0.3in}chg$f_{bc}$ $v$ $g$ = \textbf{case} $v$ \textbf{of}\\
\hspace{0.5in}\bracea{} B $a$ $f$ $\rightarrow$ B $a$ ($g$ $f$); C $f$ $a$ $\rightarrow$ C ($g$ $f$) $a$ \bracez{}\\
\hspace{0.3in}has$f_{bc}$ $v$ = \textbf{case} $v$ \textbf{of}\\
\hspace{0.5in}\bracea{} B \_ \_ $\rightarrow$ \textbf{true}; C \_ \_ $\rightarrow$ \textbf{true}; A \_   $\rightarrow$ \textbf{false} \bracez{}\\
\end{flushleft}
}

The translation shows how the generated field functions look like. The names of the \emph{upd...}, 
\emph{chg...} and \emph{has...} functions can not be mentioned directly by the programmer, 
as they are picked by the compiler in order to avoid name clashes. 
There exist suitable  \hyperref[primexp]{primary expressions} to obtain and use the functions, though.


\subsubsection{Type Namespaces} \label{tdnr}

Each declaration of a data type $T$ $u_1$ $\cdots$ $u_k$ with $k \ge 0$ creates also a new namespace. 
This namespace will be populated with the declarations in the optional \term{where} clause of the \term{data} declarations.
Each item $v$ declared in the \term{where} clause of data type $T$ $u_1$ $\cdots$ $u_k$  can be accessed with the qualified name $T$.$v$ and, 
as explained in \autoref{memfunapp}, 
if $e$ is of type $T$ $u_1$ $\cdots$ $u_k$, 
then the expression $e$.$v$ is equivalent to ($T$.$v$ $e$).

We call this feature \emph{type directed name resolution} and it applies to algebraic datatypes as well as \hyperref[nativedat]{native ones}. To obtain best results, the type checker collects not yet resolved names of a top level function in the form of type constraints, and tries to solve them all at once before the final type gets inferred.
However, unlike with type class constraints, unsolved name resolutions are not allowed and thus never appear in the type of a top level function.

\hasdiff{
\begin{itemize}
\item Field names live in the namespace that is associated with the constructed type and are not global.
\item Several forms of \hyperref[primexp]{primary expressions} deal with extraction, update and change of fields.
\item Infix notation cannot be used in constructor declarations.
\item No constraints can be given for constructors.
\item There is no \term{deriving} clause. A \hyperref[derivedcl]{derive declaration} can be used instead.
\item A data type with exactly one constructor that has exactly one field serves the same purpose as a \term{newtype} declaration.
\end{itemize}
}


\subsection{Native Datatype Declaration} \index{data type} \index{data type!native} \index{data type!user defined} \label{nativedat}

\begin{flushleft}
\rul{datadcl} \term{data} \nont{conid} \some{\nont{tyvar}} \sym{=} \term{mutable native} \nont{nativeitem} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}
\alt \term{data} \nont{conid} \some{\nont{tyvar}} \sym{=} \term{pure native} \nont{nativeitem} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}
\alt \term{data} \nont{conid} \some{\nont{tyvar}} \sym{=} \term{native} \nont{nativeitem} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}\\
\rul{nativename} \nont{varid}
  \alt \nont{conid}
  \alt \nont{varid} \sym{.} \nont{nativename}
  \alt \nont{conid} \sym{.} \nont{nativename}
\end{flushleft}

A native data type declaration \texttt{data} $T$ $u_1$ $\cdots$ $u_k$ $=$ \texttt{native} $N$ introduces a new type constructor $T$ that is associated with the \java{} type $N$. $T$  $u_1$ $\cdots$ $u_k$ is to \frege{} an abstract data type. $N$ may be a primitive java type like \texttt{int} or any java reference type. It is required to use fully qualified \java{} names for the latter.

The three syntactic forms help to distinguish between mutable and immutable (pure) data types, 
and data types whose values can be regarded as immutable under certain circumstances and mutable in others. 
Truly immutable objects are rare in \java{}, so in most cases the \term{pure native} form will not be the appropriate one. A deeper discussion of this matters can be found in \autoref{mutable-immutable-data}.

For convenience, \java{} type names can be specified without quotes, as long as the components are valid \frege{} identifiers. This excludes names starting with underscores or names that contain the \$ sign and also \java{} generic type expressions like \texttt{java.util.List<Integer>}. Such \java{} types must be specified in the form of a string literal.

The generated code will contain the native type string and this will make the \java{} compiler complain if something is not in order.

Note that \texttt{void} is not a valid native type name since \texttt{void} is not a proper type.

For one and the same native type, more than one native data type declaration can exist. Because every reference type is its own supertype, the type checker will not regard those types as different (see also \autoref{polymorphism}).

Native data types can be used like any other type, for example, they can serve as building blocks for algebraic data types, or be parts of function types. However, since there is no constructor nor any knowledge about the implementation of the type, no pattern matching on values of native data types is possible. Basic operations on the type can be introduced with \hyperref[nativefun]{native function declarations}.

\frege{} borrows all fundamental data types like characters, numbers, booleans and strings from \java{} via native data type declarations. 

\subsubsection{Support for \java{} Class Hierarchy} \label{polymorphism}

The \frege{} type checker takes into consideration the subclass relations between \java{} types. If $T_1$ and $T_2$ are type constructors of the same kind that are associated with \java{} class or interface types $C_1$ and $C_2$, and if $C_2$ is a super class of $C_1$ or an interface implemented by $C_1$, directly or through inheritance, then a type application $T_1$ $a_1 \cdots{} a_n$ can appear wherever $T_2$ $a_1 \cdots{} a_n$ is expected.

In addition, in the translation of an expression of the form $e.m$ where $e$ has a type $T a_1 \cdots{} a_n$ and $T$ is associated with a native type $C$, not only the name space $T$ is searched for $m$, but all name spaces of all known types that are associated with supertypes of $C$.

\subsection{Type Synonyms} \label{typedcl} \index{declaration!top level!type synonym}

\begin{flushleft}
\rul{typdcl} \term{type} \nont{conid} \some{\nont{tyvar}} \sym{=} \nont{sigma}
\end{flushleft}

A type synonym has the form
\begin{quote}
\texttt{type} $T$ $u_1$ $\cdots$ $u_k$ = $t$
\end{quote}
where $k\ge 0$ and the $u_i$ are the type variables occurring in the type expression $t$. It is a static error if $t$ contains a free type variable not listed on the left hand side among the $u_i$. 

A type synonym $T_a$ depends on another type synonym $T_b$ if its right hand side mentions $T_b$ or another type synonym $T_c$ that in turn depends on $T_b$.

It is a static error if a type synonym $T$ depends on itself.
This means that cyclic definitions like \exq{
type T a = (a, X a)\\
type X a = T a\\}
are forbidden.

A type expression ($T$ $t_1$ $\cdots$ $t_k$) where $T$ is a type synonym is equivalent to the type expression $t$ of the right hand side of the declaration of $T$ where each variable $u_i$ in $t$ is replaced by the type expression $t_i$. Type synonyms cannot be partially applied in type signatures, it is a static error if during typechecking a type synonym declared with $k$ type variables is found, that is applied to less than $k$ type arguments. However, it is not required that the right hand side of a type synonym declaration is a type of kind \sym{*}; expansion may produce a partially applied type constructor:

\begin{code}
data T key value = T [(key, value)]
type X = T String

foo :: X Int
foo = [("x", 42)]
\end{code}

In the example above, expansion of type \texttt{X} produces a partially applied type constructor; to form a type one more argument is required.

Type synonyms are most often used to make type expressions more readable and programs more maintainable.

\subsubsection*{Liberalized Type Synonyms}

Unlike in \haskell{} 2010, the right hand side of a type synonym may be a forall type or a constrained type. Consequently, one can write:

\begin{code}
type Discard a = forall b. Show b => a -> b -> (a, String)

f  :: Discard c
-- :: forall b c. Show b => c -> b -> (c, String)
f x y = (x, show y)

g  :: Discard Int -> (Int,String)    -- A rank-2 type
-- :: (forall b . Show b => Int -> b -> (Int, String)) -> (Int, String) 
g f = f 3 true
\end{code}

Such liberalized type synonyms may not be used where the right hand side - if written literally - would not be allowed. For example, given the definition above, the following annotation is invalid, because it applies the synonym at a place where only ordinary types are allowed:

\begin{code}
h :: Int -> Maybe (Discard Int)    -- illegal type argument (Discard Int)
\end{code}



\section{Type Classes and Overloading}
\subsection{Class Declarations} \label{classdcl} \index{class!declaration} \index{declaration!top level!class}

\begin{flushleft}
\rul{classdcl} \term{class} \nont{conid} \opt{\nont{constraints} \sym{=>}} \nont{classvar} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}\\
\rul{classvar}  \nont{varid}
\end{flushleft}

A \emph{class declaration} introduces a new class and the operations (\emph{class methods}) on it. A class declaration has the general form:

\begin{quote}
\texttt{class} $C$ \hspace{0.2cm} ($S_1$ $u$,$\cdots$,$S_k$ $u$)  $=>$ $u$\hspace{0.2cm} \texttt{where} \hspace{0.2cm} \emph{decls}
\end{quote}

This introduces a new class name $C$ with class variable $u$ and so called superclasses $S_i$.

A class variable stands for potential types that will be instances of the type class. It is also possible that the class variable is higher kinded, i.e. that it is applied to other types in the class operation annotations. The kind of the class variable must be the same in all class operations and in all superclasses.

The $S_i$ denote the superclasses of $C$.
The superclass relation must not be cyclic. If $S$ is a superclass of $C$, then each type that is an instance of $C$ must also be an instance of $S$.

The class declaration introduces new \emph{class methods} in its \emph{decls} part.
The class methods are not only visible in the scope of the class, but also at the top (module) level.
Consequently, a class method can not have the same name as a top level definition or another class method.

A class method declaration is either

\begin{itemize}
\item a new operation introduced with a \hyperref[annotation]{type annotation}. The type given must mention the class variable and the class variable must not be constrained.

Optionally, a definition of the method can be given. The definition serves as a default implementation and will be used in instance definitions that give no instance specific implementation of that method.

A \hyperref[nativefun]{native function} is annotation and definition in one declaration, so this too is allowed. This especially makes sense when one models \java{} inheritance hierarchies with type classes.

\item a definition of one of the class methods of a superclass. There must be no annotation for such methods. The type of the class method will be derived from that of the superclass method by replacing the superclasses' class variable with the current class variable.
\end{itemize}

No other declarations are permitted in the \emph{decls} part of a \texttt{class} declaration.

A \texttt{class} declaration without \texttt{where} clause is equivalent to one with an empty \emph{decls} part.
This can be useful for combining a collection of classes into a larger one that inherits all of the class methods in the original ones.
Nevertheless, even if a type is an instance of all the superclasses, it is not \emph{automatically} an instance of the new class. An instance declaration (with no \texttt{where} clause) is still required to make it one.

The same holds for types that happen to have implementations for all the operations of  a class. That does not make them automatically instances of the class: there is no class membership without an instance declaration.

\paragraph*{Example} We give here a simplified version of some classes declared in the standard Prelude.
See also \autoref{std-classes}.

\label{classexample}
\begin{code}
class Eq eq where
    (==) :: eq -> eq -> Bool
    (!=) :: eq -> eq -> Bool
    hashCode :: eq -> Int
    a != b  =  if a == b then false else true

class Ord Eq ord => ord where
    (<)  :: ord -> ord -> Bool
    ...

class Enum Ord enum => enum where
    ord   :: enum -> Int
    from :: Int -> enum
    a == b  =  (ord a) == (ord b)
    ...
\end{code}

The \texttt{Eq} class introduces two new overloaded operations and the function \texttt{hashCode}, 
with a default implementation for the \texttt{(!=)} method that makes use of the \texttt{(==)} operation. 
The \texttt{Ord} class is a subclass of \texttt{Eq} and introduces more relational operations. 
The \texttt{Enum} class is declared as subclass of \texttt{Ord} and this makes it automatically also a subclass of \texttt{Eq}. 
Therefore, it is possible to give a default implementation for the \texttt{(==)} method. 

\subsection{Instance Declarations} \label{instdcl} \index{instance!declaration} \index{declaration!top level!instance}

\begin{flushleft}
\rul{instdcl} \term{instance} \nont{classname}  \opt{\nont{constraints} \sym{=>}} \nont{type} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}
\end{flushleft}

An \emph{instance declaration} introduces an instance of a class. Let
\begin{quote}
\texttt{class} $C$ $u$ \texttt{where \{} \nont{cbody} \texttt{\}}
\end{quote}
be a class declaration.
The general form of the corresponding instance declaration is:
\begin{quote}
\texttt{instance} $C$ ($X_1$ $t_a$,$\cdots$,$X_n$ $t_b$) \sym{=>} $T$ $t_1$ $\cdots$ $t_k$ \texttt{where \{} \nont{decls} \texttt{\}}
\end{quote}
where $k,a,b \ge 0$, $a,b \le k$ and $n \ge 0$. 

If $T$ is a type synonym, the expansion of the type expression must eventually lead to a type application of a type constructor\footnote{Note that a function type like $a \rightarrow{} b$ is an application of type constructor
\sym{(}$\rightarrow{}$\sym{)}}. Otherwise, $T$ itself is already a type constructor. The type expression $T$ $t_1$ $\cdots$ $t_k$ must have the same kind as the class variable of $C$.

An instance declaration may place arbitrary constraints $X_1$ $\cdots$ $X_n$ on all or some of the types represented by the type variables $t_1$ $\cdots$ $t_k$. For example

\example{
instance Eq  (Eq a) \sym{=>} [a] where ...
}

states that for a list type to be an instances of $Eq$, the list elements themselves must be of a type that is an instance of $Eq$. This is another way to say that in order to check list equality, one must be able to check equality on list elements also.

In this example, the instantiated class and the class mentioned in the constraint are the same. This is caused by the logic of relational operations, but is not a language requirement. Any other class could be mentioned as well.

There may be at most one instance per type class and type constructor. Because of this restriction, it is usually a good idea to design the instance as general as possible. The most general case is when the $t_i$ are all distinct type variables.

\example{

\begin{tabular}{ll}
    class C this where ... & \\
    instance C [Int] where ...   & -- ok, but quite restrictive\\
    instance C [a]   where ... & -- ERROR, [] is already an instance of C\\
    instance C (a,a) where ... & -- ok, but restricted\\
    instance C (a,b,c) where ... & -- most general instance\\
\end{tabular}

}

\hasdiff{The arguments to a type constructor need not be distinct type variables.

Type synonyms in instance declarations are allowed.

}

\paragraph*{Instance methods}
Instance specific bindings of class methods and not yet implemented superclass methods are searched in the scope of the instantiated type and in the instance declarations $decls$.
It is an error if both sources contain a binding for a class method. It is also an error if none of them contains such a binding unless  there is a default implementation.

Annotations may be given; they will be checked to match the computed type of the instance method.
This type is obtained by substituting the type expression describing the instantiated type for every occurrence of the class variable in the annotation of the class method. In addition, during type check, it will be checked that the definition of the instance method indeed has the computed type, as usual.

It is also possible to implement a class method with a \hyperref[nativefun]{native function}.

If a class method has a default implementation but no instance specific implementation is found, the source code of the default implementation is taken to construct an instance specific implementation.

Each implementation of a class method that comes from the instance declarations or from a default implementation is linked back to the namespace of the instantiated type. This is so that the implementations of class operation \emph{classop} specific for type $T$ can be accessed under the qualified name $T$.\emph{classop}.


\paragraph{Instantiating a Class Hierarchy with a single instance declaration.} It is possible to declare an instance for a subclass and hence to make the instantiated type also an instance of all superclasses without giving explicit instance declarations for the superclasses, provided that
\begin{itemize}
\item the instance declaration contains implementations for the required class methods of the superclasses or
\item the subclass gives default implementations for the superclasses' required methods.
\end{itemize}
For example, the type class \texttt{Enum} is a subclass of \texttt{Ord}, which is in turn a subclass of \texttt{Eq}.
\texttt{Eq} requires definitions for \term{hashCode} and \term{==}.
\texttt{Ord} requires a definition for  \term{<=>}.
\texttt{Enum} has a default implementation for \texttt{(Eq.hashCode)} and \texttt{(Ord.<=>)}.
\texttt{Ord} has a default implementation for \texttt{(Eq.==)} in terms of \texttt{(Ord.<=>)}.
Class \texttt{Eq} itself has a default implementation for \texttt{(Eq.!=)}.
Thus it is possible to declare  \texttt{Enum} instances without caring about the \texttt{Eq} and \texttt{Ord} methods.
But because \texttt{Ord} has no implementation for \texttt{(Eq.hashCode)} one must provide one if one defines an \texttt{Ord} instance without there being also a \texttt{Eq} instance.

\note{If $A$ is a superclass of both $B$ and $C$, it is not valid to have just instances for $B$ and $C$, but not $A$ for some type $T$ in a module, because the order instance declarations are processed is unpredictable. It is only guaranteed that instance declarations for any class are processed before instance declarations for its subclasses. Because $T$-specific implementations for $A$s methods can only be given, explicitly or implicitly, in either the instance declaration for $B$ or that for $C$, the validity of the program depends on the order of processing. Hence the correct thing to do is to instantiate $A$, $B$ and $C$.}

\subsection{Derived Instances} \label{derivedcl}

For the Prelude classes \texttt{Eq}, \texttt{Ord}, \texttt{Enum}, \texttt{Bounded} and \texttt{Show} it is possible to \emph{derive} instances automatically.

\begin{flushleft}
\rul{derivedcl} \term{derive}  \nont{classname}  \opt{\nont{constraints} \sym{=>}} \nont{type} 
\end{flushleft}

Derived instances provide convenient commonly-used operations for user-defined data types.
For example, derived instances for data types in the class \texttt{Eq} define the operations \texttt{==} and \texttt{!=}, freeing the programmer from the need to define them. The precise details of how
the derived instances are generated for each of these classes are given in \autoref{derived},
including a specification of when such derived instances are possible.

\trans{
A valid \texttt{derive} declaration is translated like this:\\
\begin{tabular}{ll}
\textbf{derive} & $C$ ($X_1$ $t_a$,$\cdots$, $X_n$ $t_b$) \sym{=>} $T$ $t_1$ $\cdots$ $t_k$ $=$ \\
& \textbf{instance} $C$ ($X_1$ $t_a$,$\cdots$, $X_n$ $t_b$) \sym{=>} $T$ $t_1$ $\cdots$ $t_k$ \\
& \hspace{1cm}\textbf{where \{} $decls_C$ \textbf{\}}\\
\textbf{derive} & $C$ $T$ $t_1$ $\cdots$ $t_k$ $=$ \\
& \textbf{instance} $C$ ($C$ $t_1$,$\cdots$, $C$ $t_k$) \sym{=>} $T$ $t_1$ $\cdots$ $t_k$ \\
& \hspace{1cm}\textbf{where \{} $decls_C$ \textbf{\}}\\
\end{tabular}
\par where $decls_C$ are compiler generated declarations whose concrete content depends on $C$ and the structure of $T$  $t_1$ $\cdots$ $t_k$.
}

As with instance declarations, it is possible to specify constraints in derive declarations. The constraints so given must contain the set of constraints  ($C$ $t_1$,$\cdots$, $C$ $t_k$) where $C$ is the derived class and  the $t_i$ are the type variables of the instantiated type. If, however, no constraints at all are given, the constraints needed will be silently supplied by the compiler.


\subsection{Ambiguous Types}

A problem inherent with overloading is the possibility of an \emph{ambiguous type}.
For example, using the \emph{from} and \emph{ord} functions from the \emph{Enum} class introduced in the last section, then the following declaration
\exq{amb x = if ord (from 1) == 1 then x else x+x}
causes the type inference algorithm to attribute the type
\exq{(Enum b,Num a) \sym{=>} a $\rightarrow$ a}
to \emph{amb}. If such type were allowed, it would never be possible to decide at which type to instantiate type variable $b$ which is totally unrelated to type variable $a$ which stands for the argument's type. Therefore, such types are considered ill-typed and programs containing them are rejected.

We say that an expression has an ambiguous type if, in its type 
\exq{\textbf{forall} $u_1$, $\cdots$, $u_k$ \sym{.} $cx$ \sym{=>}  $t$ }
there is a type variable $u_j$ that occurs in $cx$ but not in $t$.

Ambiguous types can only be circumvented by input from the user. One way is through the use of expression
type-signatures as described in \autoref{annex}. Our example could be rewritten as follows:
\exq{amb x = if ord (from 1 :: Bool) == 1 then x else x+x}

\section{Nested Declarations} \label{decl}

The declarations described here can appear at the top level or in the scope of a class  declaration, instance declaration or datatype declaration. With the exception of the \hyperref[nativefun]{native function declaration} they can also appear in a \hyperref[letexpr]{\texttt{let} expression}. In fact, this are the only declarations allowed in \texttt{let} expressions and \texttt{where} clauses that are part of expressions. (Such \texttt{where} clauses will be transformed to \texttt{let} expressions ultimately.)

\begin{flushleft}
\rul{decl} \nont{annotation} \gcom{Type Annotation}
  \alt \nont{binding}        \gcom{Function or Pattern Binding}
  \alt \nont{nativefun}      \gcom{Native Function Declaration}
\end{flushleft}

\subsection{Type Annotations} \label{annotation}

A \emph{type annotation} specifies the type of a variable.

\begin{flushleft}
\rul{annotation} \liste{\nont{annoitem}}{,} \sym{::} \nont{sigma}\\
\rul{annoitem} \nont{varid} \oder{} \nont{symop} \oder{} \nont{unop}
\end{flushleft}

\trans{An annotation with more than one item is translated to $k$ annotations, where $k$ is the number of annotated items.
\begin{flushleft}
$a_1$, $\cdots$, $a_k$ \sym{::} $s$\\
\hspace{0.5cm} $=$\\
$a_1$ \sym{::} $s$\\
\hspace{0.5cm}$\cdots$\\
$a_k$ \sym{::} $s$\\
\end{flushleft}
}

A type annotation has the form
\begin{quote}
$v$ \texttt{::} $t$
\end{quote}
where $v$ is the annotated item which may be a variable or an unary or binary operator symbol. (To simplify matters, we use the term \emph{variable} in place of \emph{annotated item} in the discussion that follows.)

Except for class methods, annotated variables $v$ must have also a value binding, and the binding must appear in the same declaration list that contains the type signature; i.e. it is invalid
to give a type signature for a variable bound in an outer scope. Moreover, it is invalid to give more than one type signature for one variable, even if the signatures are identical.

As mentioned in \autoref{typesyntax}, every type variable appearing in a signature is universally quantified over that signature, and hence the scope of a type variable is limited to the type expression that contains it.
For example, in the following declarations \exq{
f :: a -> a \\
f x = x :: a -- invalid \\
}
the \texttt{a}'s in the two type expressions are quite distinct.
Indeed, these declarations contain a static error, since \texttt{x} does not have type $\forall$ $a$.$a$ but is dependent on the function type.

If a given program includes a signature for a variable $f$ , then each use of $f$ is treated as having the declared type.
It is a static error if the same type cannot also be inferred for the defining occurrence of $f$.

If a variable $f$ is defined without providing a corresponding type signature declaration, then each use of $f$ outside its own declaration group (see \autoref{declgroup}) is treated as having the corresponding inferred, or \emph{principal} type.
However, to ensure that type inference is still possible, the defining occurrence, and all uses of $f$ within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in \autoref{generalization}).

For example, if we define \exq{
sqr x = x*x}
then the principal type is \texttt{sqr} :: \textbf{forall} $a$.\texttt{Num} $a$ \sym{=>} $a \rightarrow{} a$, which allows applications such as \texttt{sqr 5} or \texttt{sqr 0.1}.
It is also valid to declare a more specific type, such as \exq{
sqr :: Int $\rightarrow$ Int} but now applications such as \texttt{sqr 0.1} are invalid. Type signatures such as \exq{
sqr :: (Num a, Num b) \sym{=>} a $\rightarrow$ b\\
sqr :: a $\rightarrow$  a} are invalid, as they are more general than what is warranted by the definition.

However, there are certain cases where the type checker infers a type that is not the most general one possible for the definition given. In such cases, an annotation can be used to specify a type more general than the one that would be inferred. Consider this rather pathological example:
\begin{code}
data T a = K (T Int) (T a)
f :: T a -> a
f (K x y) = if f x == 1 then f y else undefined
\end{code}
If we remove the annotation, the type of \texttt{f} will be inferred as \texttt{T Int -> Int} due to the first recursive call for which the argument to \texttt{f} is \texttt{T Int}.

To sum it up, there are the following possible uses of type annotations:
\begin{enumerate}
\item Declaration of a new class method, as described in \autoref{classdcl}.
\item Declaration of a more restricted type than the principal type.
\item Declaration of a more general type than the inferred type. Please observe that, even if the type inference algorithm is not able to infer the most general type from a definition, it is still able to check whether the type signature supplied is valid. Therefore, type annotations cannot be used to lie about the type of a variable.
\item Declaration of a type that is identical to the type that would have been inferred. This may be useful for documentation purposes.
\item Declaration of a polymorphic type for \hyperref[generalization]{let bound functions}.
\item Declaration of a \hyperref[higher-rank]{higher ranked type}.
\end{enumerate}


\subsection{Function and Pattern Bindings} \label{binding}

\begin{flushleft}
\rul{binding} \nont{lhs} \nont{rhs}\\
\rul{lhs} \nont{funlhs} \oder{} \nont{pattern}\\
\rul{funlhs} \nont{varid} \more{\nont{pterm}}
  \alt \nont{pconapp} \nont{lexop} \nont{pconapp}\\
\rul{rhs} \sym{=} \nont{expr} \opt{\term{where} \bracea{} \nont{decls} \bracez{}}
  \alt \nont{guarded-exs}  \opt{\term{where} \bracea{} \nont{decls} \bracez{}} \gcom{see \autoref{caseex} for syntax of \nont{guarded-exs}}
\end{flushleft}

We distinguish two cases of value bindings: If the left hand side is neither a constructor application nor an application of the unary operator \texttt{!} or the pattern name binding operator \texttt{@}\footnote{These exceptions in an already complicated rule can only be justified by the fact that one seldom wants to redefine the \texttt{!} or \texttt{@} functions.}, and if it can be interpreted as a variable applied to one or more patterns, or as a binary operator except \texttt{@} applied to two patterns in infix notation, we call it a function binding, otherwise it is a pattern binding. Thus, a left hand side like $m$\symbol{126}\#$re$\#, though making a valid pattern, will be treated as function binding (i.e. definition of the operator  \texttt{\symbol{126}}). On the other hand, $x$:$xs$, \bracka{}$a$, $b$\brackz{} and ($a$, $b$) are pattern bindings, since all three just employ special syntax for constructor applications, \texttt{!}$x$ is a (strict) pattern binding and $qs$\texttt{@}$q$:\_ is a pattern binding for a list $qs$ with head $q$ and an unnamed tail. Finally, a simple variable or an operator enclosed in parentheses is a pattern binding for that name.

\subsubsection{Function bindings} \label{fundef}

A function binding binds a variable (or operator) to a function value.
The general form of a function binding for variable $x$ is:
\begin{quote}
\begin{flushleft}
$x$ $p_{11}$ $\cdots$ $p_{1k}$ $match_1$\\
$\cdots$\\
$x$ $p_{n1}$ $\cdots$ $p_{nk}$ $match_n$\\
\end{flushleft}
\end{quote}
where $k\ge 1$, $n\ge 1$ and each $p_{ij}$ is a pattern and the matches $match_i$ are just like the matches in \hyperref[caseex]{case expressions}.

All clauses defining a function must be contiguous, and the number of patterns in each clause must be the same. The set of patterns corresponding to each match must be linear, that is, no variable is allowed to appear more than once in the set.

\trans{The general binding form for functions is semantically equivalent to the equation
\begin{flushleft}
$x$ = $\backslash{}x_1 \cdots{} \backslash{}x_k \rightarrow{} $\textbf{case} $(x_1, \cdots, x_k)$ \textbf{of}\\
\hspace{2cm}$(p_{11}, \cdots, p_{1k})$ $match_1$\\
\hspace{2cm}$\cdots$\\
\hspace{2cm}$(p_{n1}, \cdots, p_{nk})$ $match_n$\\
\end{flushleft}
where the $x_i$ are new identifiers.
}

Note that several clauses defining a function count as a single  declaration. While definitions of different functions may appear in any order without changing the meaning of the program, this is not true for the clauses of a function definition. On the contrary, because of the translation given above and the semantics of \texttt{case} expressions, their order is quite important and cannot usually be changed without changing also the meaning of the program.

\subsubsection{Pattern bindings} \label{patdef}

A \emph{pattern binding} binds all variables contained in the pattern on the left hand side to values. It is a static error if the pattern does not contain any variables. The pattern is matched against the expression on the right hand side only when one of the bound variables needs to be evaluated. In any case, the expression on the right hand side will be evaluated at most once, and for each bound variable the match is performed at most once.

This default lazy semantics can be overridden by using strict patterns (see page \pageref{strictpats}). A strict variable will be evaluated as soon as it is bound to a value. This may cause other variables on which the strict variable depends to be evaluated, too.

A \emph{simple} pattern binding has the form $v$ = $e$, where $v$ is just a variable. No actual pattern matching is needed in this case. The evaluation of $v$ will cause evaluation of $e$ and the resulting value is the value of $v$. If $v$ is not evaluated, $e$ will also not be evaluated.

The \emph{general} form of a pattern binding is $p$ $match$, where $match$ is the same structure as for function bindings above, which in turn is the one used in case expressions; in other words, a pattern binding is:
\begin{quote}
\begin{flushleft}
$p$ $|$ $g_1$ = $e_1$ $|$ $g_2$ = $e_2$ $|\cdots$ $|$ $g_m$ = $e_m$\\
\hspace{0.3cm}\textbf{where} \{ $decls$ \}
\end{flushleft}
\end{quote}
\trans{The general pattern binding above is semantically equivalent to the following:
\begin{flushleft}
$x$ = \textbf{let} \{ $decls$ \} \textbf{in}\\
\hspace{1cm}\textbf{case} () \textbf{of} \{ () $|$ $g_1$ = $e_1$ $|$ $g_2$ = $e_2$ $|\cdots$ $|$ $g_m$ = $e_m$ \}\\
$v_1$ = \textbf{case} $x$ \textbf{of} \{ $p \rightarrow{} v_1$ \}\\
$\cdots$\\
$v_k$ = \textbf{case} $x$ \textbf{of} \{ $p \rightarrow{} v_k$ \}\\
\end{flushleft}
where $k\ge 1$ and the $v_i$ are the variables occurring in the pattern $p$ and $x$ is a variable not used elsewhere.
}

\subsection{Static Semantics of Function and Pattern Bindings} \label{letsemantics}

The static semantics of the function and pattern bindings of a \texttt{let} expression or \texttt{where} clause are discussed in this section.

\subsubsection{Dependency Analysis} \label{declgroup}

In general the static semantics are given by the normal Hindley-Milner inference rules.
A \emph{dependency analysis} transformation is first performed to simplify further processing.
Two variables bound by value declarations are in the same \emph{declaration group} if their bindings are mutually recursive (perhaps via some other declarations that are also part of the group).

Application of the following rules causes each \texttt{let} or \texttt{where} construct (including the (implicit) \texttt{where} defining the top level bindings in a module) to bind only the variables of a single declaration group, thus capturing the required dependency analysis:

\begin{enumerate}
\item The order of function and pattern bindings in \texttt{where}/\texttt{let} constructs is irrelevant.
\item \textbf{let} \{ $d_1$; $d_2$ \} \textbf{in} $e$ transforms to \textbf{let} \{ $d_1$  \} \textbf{in} \textbf{let} \{ $d_2$ \} \textbf{in} $e$ when no identifier bound in $d_2$ appears free in $d_1$.
\end{enumerate}

\subsubsection{Generalization} \label{generalization}

The type system assigns types to a \texttt{let}-expression in two stages.
First, the right-hand sides of the declarations are typed, giving types with no universal quantification.
Second, if and only if the local declaration had a type annotation, the annotation is checked and a generalized type is attributed to the binding.
Finally, the body of the \texttt{let}-expression is typed.

\hasdiff{In \frege{}, un-annotated let bound declarations are not generalized. If one wants polymorphic local functions, one needs to provide a type signature.}

For example, consider the declaration \exq{
f = let g y = (y,y) in (g true, g 0)
}
that would be valid in other languages with Hindley-Milner type system.
The type of \texttt{g}'s right-hand side is $a \rightarrow{} (a,a)$. A generalization step would attribute to \texttt{g} the polymorphic type $\forall a. a \rightarrow{} (a,a)$, after which the typing of the body part can proceed. This makes \texttt{g} independent of any other types and allows its usage in the body at \emph{different} types.

In \frege{}, however, this generalization step has been deliberately omitted. The rationale for this is:
\begin{itemize}
\item As Simon Peyton Jones argues in \cite{lsnbg}:
\begin{quote}
... generalisation for local let bindings is seldom used; that is; if they are never generalised, few programs fail to typecheck ... We base this claim on compiling hundreds of public domain Haskell packages, containing hundreds of thousands lines of code. Furthermore, those programs that do fail are readily fixed by adding a type signature.
\end{quote}
\item Generalisation affects type constraints that arise from the use of type class operations. This means that type class constraints must be passed to local functions at runtime, and the associated operations can only be performed indirectly. Consider the following example: \exq{
f = (dbl 7, dbl 13) where dbl x = x+x
}
Here, the \texttt{dbl} function is only used at type \texttt{Int}, and without generalisation we can simply generate \java{} code like: \exq{
public int dbl(final int x) \{ return x+x; \}
}
But with generalisation, \texttt{dbl} gets the type:  $\forall a.$ Num $a => a \rightarrow{} a$ and we need something like \exq{
public Object dbl(CNum ctx, Object x) \{ \\
       return ctx.plus().apply(x).apply(x).result(); \}
}
which results in at least 4 object creations.
\item \hyperref[tdnr]{Type directed name resolution} also benefits, as the type of some data may be exposed in some let bound function or list comprehension (which is desugared to a series of let definitions), but this knowledge will not be usable in other let bound functions when their type is generalized.
\end{itemize}

Sometimes it is not possible to generalize over all the type variables used in the type of the definition. For example, consider the declaration  \exq{
f x = let g z y = ([x,z],y) in ...
}
In an environment where \texttt{x} has type $a$, the type of \texttt{g}'s defining expression is $a \rightarrow{} b \rightarrow{} ([a],b)$. In this case, only $b$ could be universally quantified because $a$ occurs in the type environment. We say that the type of \texttt{g} is \emph{monomorphic in the type variable a}.

The effect of such monomorphism is that the first argument of all applications of \texttt{g} must be of a single type. For example, it would be valid for the "..." to be \exq{
(g true 0, g false 1)}
(which would, incidentally, force \texttt{x} to have type \texttt{Bool}) but invalid for it to be \exq{
(g true 0, g 'c' 1)}

It is worth noting that the explicit type signatures provided by \frege{} are not powerful enough to express types that include monomorphic type variables.
For example, we cannot write
\begin{code}
    f x = let
            g :: a -> b -> ([a],b)
            g y z = ([x,y], z)
        in ...
\end{code}
because that would claim that \texttt{g} was polymorphic in both \texttt{a} and \texttt{b}. In this program, \texttt{g} can only be given a type signature if its first argument is restricted to a type not involving type variables; for example \exq{
g :: Int -> b -> ([Int],b)}
This signature would also cause the variable \texttt{x} to have type \texttt{Int}.

\subsubsection{Higher Rank Polymorphism} \label{higher-rank}

In the Hindley-Milner type system, the types of lambda bound variables are always monomorphic. This restriction keeps type inference decidable, but excludes \emph{higher rank polymorphism}, that is, the ability to write functions that take polymorphic functions as arguments. For an in depth discussion of these matters see \cite{ptifart}. The conservative extension of the type system proposed in that paper is  implemented in the \frege{} type system.

To exemplify the problem, consider the following program:

\begin{code}
foo :: ([Bool], [Char])
foo = let
        f x = (x [true,false], x ['a','b','c'])
    in f reverse
\end{code}

In the body of \texttt{f}, the function \texttt{x} is applied both to a list of booleans and a list of characters - but that should be fine because the function passed to \texttt{f}, namely \texttt{reverse} (a library function with type $\forall{} a$.$[a] \rightarrow{} [a]$) works equally well on lists of any type. Nevertheless, the expression is rejected as it stands. With the restriction on lambda bound arguments, the type checker can assign to \texttt{x} the type \texttt{[Bool] -> [Bool]} or \texttt{[Char] -> [Char]} but not $\forall{} a$.$[a] \rightarrow{} [a]$.

The \frege{} type checker can overcome this restriction of the Hindley-Milner type system with the help of user supplied type annotations. In our case, there are two opportunities to suggest the correct type for the argument $x$:
\begin{enumerate}
\item One could annotate the pattern $x$ with the type 
\exq{\textbf{forall} $a$.[$a$] $\rightarrow{}$ [$a$]}
\item One could annotate $f$ itself with 
\exq{(\textbf{forall} $a$.[$a$] $\rightarrow{}$ [$a$]) $\rightarrow$ ([Bool], [Char])}
\end{enumerate}

If one chooses the former, the example above looks then like

\begin{code}
foo :: ([Bool], [Char])
foo = let
        -- f will take a polymorphic function as argument
        f (x::[a]->[a]) = (x [true,false], x ['a','b','c'])
    in f reverse
\end{code}

Note that we can save the \term{forall}, because the type variable $a$ scopes over the whole type of $x$.
The type checker would now be able to infer the following type for $f$:
\exq{f :: (\textbf{forall} $a$.$[a] \rightarrow{} [a]$) $\rightarrow$ ([Bool], [Char])}

Note that this is the same type one could have annotated $f$ with and that in this case the \term{forall} is crucial, as it restricts the scope of type variable $a$ to the type in parentheses. Without it, one would get
\exq{f :: ($[a] \rightarrow{} [a]$) $\rightarrow$ ([Bool], [Char])}
which is identical with
\exq{f :: \textbf{forall} $a$ \sym{.} ($[a] \rightarrow{} [a]$) $\rightarrow$ ([Bool], [Char])}
and this would mean something like: "$f$ is a function that takes as first argument a function of \emph{some unknown, albeit fixed} list type, ..." and of course neither a list of Bool nor a list of Char could be passed to this function. Whereas the former type signature with the correct placement of \term{forall} says: "$f$ is a function that takes as first argument a function that can handle \emph{any} list type, ...".

\hasdiff{Haskell 98 does not allow higher rank polymporphism, while extensions like GHC do.}

\subsection{Native  Declaration} \label{nativefun}
\index{declaration!native function}

\begin{flushleft}
\rul{nativefun} \opt{\term{pure}} \term{native} \nont{annoitem} \opt{\nont{javaitem}} \sym{::} \nont{sigma} \opt{\nont{throws}}\\
\rul{javaitem} \nont{nativename} \oder{} \nont{unop} \oder{} \nont{symop} \oder{} \nont{stringliteral}\\
\rul{throws} \term{throws} \liste{\nont{type}}{\sym{, }}
\end{flushleft}

The basic form of the \emph{native declaration}
\begin{quote}
\textbf{native} $v$  $j$ \textbf{::} $t$
\end{quote}
introduces a new variable $v$ with type $t$, that will behave like any other \frege{} variable of that type but is implemented in \java{}. $j$ is a string value that contains information regarding $v$'s \java{} implementation. For convenience, $j$ can be written without quotes as long as the names or operators specified would also be valid in \frege{}. Often, it is the case that $v$ and $j$ are the same, as in \exq{
    data String = pure native java.lang.String\\
    pure native length length :: String -> Int
}
In such cases, $j$ can simply be omitted.

The declarations above introduce the type \term{String}, which is based on the \java{} class \term{java.lang.String} and a function \term{length} that takes a value of type \term{String} and returns an \term{Int}
\footnote{The declarations shown here for demonstration are actually part of the standard library and hence available in every frege program.}. 
This function is implemented with an instance method \term{length}. Because a \java{} instance method needs a receiver, which is by definition the first argument, and the first argument is a \term{String}, which is implemented by  \term{java.lang.String}, we can assume that an application \exq{length "foo"} will be compiled to something like \exq{"foo".length()}

The \frege{} compiler cannot check the validity of the native declaration, only very basic sanity checks are currently possible.
 Errors not detectable (for example incorrect type information, spelling errors in identifiers, etc.) will normally cause failures during compilation of the generated \java{} code. 
The presence of invalid native declarations should be the only reason for rejection of the generated code by the \java{} compiler\footnote{Another reason would be bugs in the \java{} or \frege{} compilers}; thus whenever \texttt{javac} complains, one should first check the native declarations.

During code generation, expressions that contain native values  are mapped to certain \java{} constructs such as

\begin{itemize}
\item field access expressions (see \cite[section 15.11]{langspec3})
\item method invocation expressions (see \cite[section 15.12]{langspec3}) for both static and non-static methods
\item class instance creation expressions (see \cite[section 15.9]{langspec3})
\item unary expressions (see \cite[section 15.15]{langspec3})
\item cast expressions (see \cite[section 15.16]{langspec3})
\item binary expressions (see \cite[section 15.17 to 15.24]{langspec3})
\end{itemize}

in a transparent and well defined way. This is explained in detail in \autoref{native interface}.

\subsubsection{Overloaded native methods} \index{overloaded!native function}

The \java{} language allows \emph{overloading} of methods \cite[section 8.4.9]{langspec3}. 
Thus, in \java{} one can have different methods with the same name. 
To facilitate easy (perhaps semi-automatic) adoption of \java{} APIs in \frege{}, native functions can also be overloaded.

\begin{flushleft}
\rul{nativefun} \opt{\term{pure}} \term{native} \nont{annoitem} \opt{\nont{javaitem}} \sym{::} \liste{\nont{sigma} \opt{\nont{throws}}}{\sym{|}}
\end{flushleft}

To do this, one simply specifies the different types separated by a vertical bar.
The typechecker will check at every call site if one of the given types fits in, and it will complain if the overload cannot be resolved unanimously.

\example{\tt
\begin{flushleft}
pure native foo x.y.Z.foo :: Int -> Int | Int -> Int -> Int\\
bad = foo 3\\
good = foo 3 + 42\\
\end{flushleft}
}

In the example above, the expression for \texttt{bad} is ambiguous: \texttt{bad} could have type \texttt{Int} or \texttt{Int->Int}, therefore this would be rejected. By annotating \texttt{bad} with one of the possible types, the binding could be made valid.

In the expression given for \texttt{good}, however, the type of the application \texttt{foo 3} is certainly \texttt{Int}, as it appears as the operand of an integer addition. Hence, this overloaded use of \texttt{foo} is resolved to be at type \texttt{Int->Int}.
